\begin{tabbing}
$\forall$${\it es}$:ES, $T$:Type, $i$:Id, $P$:($T$$\rightarrow$Prop), $Q$:(E$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]($\forall$$x$:$T$. Dec($P$($x$)))
\\[0ex]$\Rightarrow$ (\=$\forall$$L$:$T$ List.\+
\\[0ex]($\forall$$x$$\in$$L$. $\forall$$e$:E. $Q$($e$,$x$) $\Rightarrow$ loc($e$) $=$ $i$ $\in$ Id)
\\[0ex]$\Rightarrow$ ($\forall$$x$$\in$$L$. $P$($x$) $\Rightarrow$ ($\exists$$e$:E. $Q$($e$,$x$)))
\\[0ex]$\Rightarrow$ ($\neg$($\exists$$x$$\in$$L$.$P$($x$)) $\Rightarrow$ $\exists$${\it e'}$@$i$.True)
\\[0ex]$\Rightarrow$ $\exists$${\it e'}$@$i$.$\forall$$x$$\in$$L$. $P$($x$) $\Rightarrow$ ($\exists$$e$:E. $e$ $\leq$ ${\it e'}$  \& $Q$($e$,$x$)))
\-
\end{tabbing}